#include "cdcl.h"
#include<mpi.h>
#include "slave_worker.h"
#include "master.h"
#include "common.h"
#include "malloc.h"
MPI_Datatype mpi_metadata_t;
//#define CDCL_SAME_CNF_DIFF_PARAM
#define CDCL_SUB_CNF_SAME_PARAM
/**
 * register mpi_metadata_t
 */
void init_mpi_datatype(){
    
    MPI_Aint offsets[2], extent, lb;
    MPI_Datatype old_types[2];
    int block_counts[2];
/**
 * typedef struct _metadata{
 *  enum MESSAGE_TYPE type;
 *  int datalen;
 * }metadata;
 */
    offsets[0] = 0;
    old_types[0] = MPI_CHAR;
    block_counts[0] = 1;

    MPI_Type_get_extent(MPI_CHAR, &lb, &extent);
    offsets[1] = extent * 4;
    old_types[1] = MPI_UNSIGNED;
    block_counts[1] = 1;

    MPI_Type_struct(2, block_counts, offsets, old_types, &mpi_metadata_t);
    MPI_Type_commit(&mpi_metadata_t);

}
extern int max_var_id;
_bool mpi_cdcl_satisfiable(cnf*_cnf, int rank){
    _bool sat = false;
    // get rank and size of processes
    int n_worker;
    MPI_Comm_size(MPI_COMM_WORLD, &n_worker);
    assert(rank < 32);
    printf("make sure rank < 32 %d\n", rank);
    max_var_id++;
    if(rank == 0){    
        //master
        master* _master;
        #ifdef CDCL_SAME_CNF_DIFF_PARAM
        _master = new_master(0, n_worker, _cnf, SAME_TASK_DIFF_TACTIC);
        #endif
        #ifdef CDCL_SUB_CNF_SAME_PARAM
        _master = new_master(0, n_worker, _cnf, TASK_APPOINT_SAME_TACTIC);
        #endif
        printf("now original cnf can use %p, \n", _cnf);
        print_cnf(_cnf);

        #ifdef CDCL_SAME_CNF_DIFF_PARAM
            start_all_worker(_master);
            printf("started all worker\n");
        #endif
        #ifdef CDCL_SUB_CNF_SAME_PARAM
            int tasknum = prepare_all_sub_tasks(_master);
            printf("inited all tasks %d\n", tasknum);
            start_all_worker(_master);
            printf("started all worker\n");
        #endif
        while (!listen_to_workers(_master));
        printf("exit listening\n");

    }
    else{
        assert(rank < 32);
        //slave
        slaveworker*slave = malloc(sizeof(slaveworker));
        #ifdef CDCL_SUB_CNF_SAME_PARAM
        {
            init_worker(slave, rank, _cnf);
            //set config
            cdcl_config config;
            switch(rank % 4){
                default:
                    config.restart_round = -1;
                    config.var_iter = true;   
                    break;        
            };
            //printf("cdclmpi rank %d: %d %d\n", rank, config.restart_round, config.var_iter);
            update_config(slave, &config);
            block_wait_for_instructions_from_master(slave);            
        } 
        #endif
        #ifdef CDCL_SAME_CNF_DIFF_PARAM
        {
            init_worker(slave, rank, _cnf);
            //set config
            cdcl_config config;
            switch(rank % 4){
                case 0:
                    config.restart_round = -1;
                    config.var_iter = true;
                    break;
                case 1:
                    config.restart_round = -1;
                    config.var_iter = false;
                    break;
                case 2:
                    config.restart_round = 300;
                    config.var_iter = true;
                    break;
                case 3:
                    config.restart_round = 300;
                    config.var_iter = false;
                    break;
                default:
                    assert(0);
            };
            //printf("cdclmpi rank %d: %d %d\n", rank, config.restart_round, config.var_iter);
            update_config(slave, &config);
            block_wait_for_instructions_from_master(slave);            
        }    
        #endif 
    }    
    return sat;
}